$\forall$$T$,$A$:Type, $f$,$g$:($T$$\rightarrow$$A$$\rightarrow$$T$), $L$:($A$ List), $y$,$z$:$T$. \\[0ex]($\forall$${\it L'}$:($A$ List), $a$:$A$. \\[0ex]iseg($A$; append(${\it L'}$; cons($a$; [])); $L$) \\[0ex]$\Rightarrow$ ($f$(list\_accum($x$,$a$.$f$($x$,$a$); $y$; ${\it L'}$),$a$) = $g$(list\_accum($x$,$a$.$f$($x$,$a$); $y$; ${\it L'}$),$a$))) \\[0ex]$\Rightarrow$ ($y$ = $z$) \\[0ex]$\Rightarrow$ (list\_accum($x$,$a$.$f$($x$,$a$); $y$; $L$) = list\_accum($x$,$a$.$g$($x$,$a$); $z$; $L$) $\in$ $T$)